|
|
Simulace pevných těles
Leitner, Denis ; Milet, Tomáš (oponent) ; Chlubna, Tomáš (vedoucí práce)
Táto práca je zameraná na simuláciu fyziky pevných telies v reálnom čase. Popisuje základné postupy používané pri hernom vývoji zamerané na detekciu kolízie medzi konvexnými mnohostenmi. Ďalej popisuje riešenie zistenej kolízie a spôsob simulácie dynamiky pevných telies. Zaoberá sa takisto aj návrhom a implementáciou simulátoru pevných telies v jazyku C++. Na vykresľovanie scény je použité OpenGL.
|
|
|
Verifikovaná knihovna datových struktur
Rychnovský, Jan ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá metodikou psaní verifikovaných programů pomocí nástroje VCC. Zmíněná metodika je založena na principu doplnění kódu programu o anotace, jež poskytují specifikaci požadované funkcionality. Nástroj VCC pak prostřednictvím formálních metod určí zda zdrojový kód splňuje danou specifikaci či ne. V první části práce je popsána formální verifikace a zmíněny tři základní přístupy k ní. Následně jsou popsány problémy splnitelnosti výrokových formulí (SAT) a splnitelnosti formulí v teoriích predikátové logiky (SMT). Práce se dále věnuje popisu verifikačního nástroje VCC, jeho funkčnosti, metodice, syntaxi a sémantice příkazů jeho anotačního jazyka BoogiePL. Druhá část textu je zaměřena na popis návrhu a implementace verifikované knihovny datových struktur obsahující jednosměrný, dvousměrný a kruhový seznam, binární vyhledávací strom a Treiberův zásobník. Závěr práce diskutuje získané poznatky o programovací metodice založené na psaní verifikovaného kódu.
|
|
|
Knihovna pro detekci kolizí
Chlubna, Tomáš ; Španěl, Michal (oponent) ; Polok, Lukáš (vedoucí práce)
Tato práce řeší problém detekce kolizí netriviálních polygonálních modelů v trojrozměrném prostoru. Obecně existují postupy, jak tyto kolize matematicky vyjádřit a vypočítat. Pro použití v oblasti informačních technologií jsou však takové metody často nepoužitelné z hlediska výkonu a paměťové náročnosti. Také oproti reálnému světu je třeba pracovat s diskrétním časem, což vede k nutnosti implementace algoritmů, schopných nejen kolize detekovat v daném časovém okamžiku, ale také je předvídat podle dostupných informací o pohybu objektů ve scéně. Návrh řešení vychází zejména z technik používaných v odvětví herního vývoje a fyzikálních simulací. V práci jsou tedy zahrnuty i mechanismy pro optimalizaci, reprezentaci scény a její vykreslování s využitím grafické karty.
|
|
| |
|
|
Vizualizace hmatových a zvukových vjemů
Lukš, Roman ; Zachariáš, Michal (oponent) ; Polok, Lukáš (vedoucí práce)
Cílem této bakalářské práce je návrh a implementace vizualizace hmatových a zvukových vjemů běžících v reálném čase. Vjemy mají sloužit pro orientaci hráče v jednoduché 2D hře místo zraku. Vjemy jsou vizualizovány pomocí shaderů na GPU. Zvukové vjemy jsou implementací simulace vlnění výpočetně nenáročnou explicitní metodou. Hmatový vjem je tvořen pomocí pohyblivých čar. K vykreslování je použita knihovna OpenGL. V práci jsem vytvořil funkční herní prototyp obsahující dvojici vjemů.
|
|
|
Využití SAT solverů v úloze optimalizace kombinačních obvodů
Minařík, Vojtěch ; Mrázek, Vojtěch (oponent) ; Vašíček, Zdeněk (vedoucí práce)
Tato práce zavádí využití řešení problému SAT a jeho modifikací v úloze evolučního návrhu kombinačních obvodů. Motivací využití těchto problémů je zrychlení ohodnocování chromozomů kandidátních řešení fitness funkcí během evoluce v případech, kdy selhává metoda klasické simulace. Využití problému SAT, respektive #SAT umožňuje oproti simulaci zrychlení zejména pro komplikované obvody s velkým počtem vstupů. Implementované řešení se zalkádá právě na problému #SAT. Celkem byly implemenyovány dvě různé varianty využití tohoto problému. Varianty se liší metodou kontorly rozdílných hodnot na výstupech obvodu. Protože implementované řešení využívá k reprezentaci obvodu logickou formuli a zkoumá její splnitelnost, časová složitost algoritmu závisí především na logické složitosti navrhovaného obvodu.
|
|
|
SAT Solver akcelerovaný pomocí GPU
Izrael, Petr ; Šimek, Václav (oponent) ; Jaroš, Jiří (vedoucí práce)
Práce se zabývá návrhem a implementací kompletního SAT solveru akcelerovaného na GPU. V první části práce je popsána architektura grafických karet a možnosti platformy CUDA. Následuje popis algoritmů a technik pro řešení problému booleovské splnitelnosti (SAT problému). Je představena zejména rodina kompletních algoritmů založených na DPLL. Právě varianta DPLL, známa jako 3SAT-DC je kompletně převedena na GPU. Práce popisuje problémy s tímto převodem spojené, stejně jako několik optimalizací a analýz. Velkým problémem je nemožnost využít v paralelním prostředí mnohé sofistikované metody známé ze sekvenčních solverů. Řešení bylo porovnáno s obdobným algoritmem implementovaným pro CPU a bylo ukázáno, že může být až 21x rychlejší. Uvedeny jsou i návrhy, jak algoritmus dále rozšířit a akcelerovat.
|
|
|
Magnetická pole pro biomedicínské experimenty
Otýpka, Jan ; Cipín, Radoslav (oponent) ; Patočka, Miroslav (vedoucí práce)
V práci se zabývám řešením magnetických polí pro využití v oboru biomedicíny. Toto řešení zahrnuje volbu správného geometrického uspořádání cívky pro generování magnetického pole s homogenním rozložením magnetické indukce v co největším možném prostoru. V práci jsou srovnány tři typy cívek tj. solenoid, toroid a Helmholtzovou cívkou. U Helmholtzovy cívky a solenoidu je pak provedený rozbor magnetické indukce ve vnitřním prostoru cívek. Další část je věnována elektrické rezonanci v LC obvodu. Ta je potom využitá pro vznik pulsního magnetického pole v Helmholtzově cívce. Jsou zde shrnuty teoretické a praktické poznatky pro návrh a konstrukci rezonančního měniče. Konec je pak věnován měření obvodových veličin a ověření teoretických poznatků.
|
|
|
Modelování kooperativního hledání cest
Ježek, Milan ; Surynek, Pavel (vedoucí práce) ; Majerech, Vladan (oponent)
V této práci jsou popsány nové modely pro řešení kooperativního hledání cest (cpf) s požadavkem na minimální makespan a je provedeno jejich experimentální porovnání se stávajícími modely. Nové modely uvedené v práci zkoumají možnosti kódování problému cpf pomocí celočíselného lineárního programování s binárními proměnnými (bip) a jako problém splnitelnosti omezujících podmínek (csp). Při testech se ukázaly hlavně poměrně dobré výsledky nového modelu IP active-edges při vyšším množství agentů, kdy jen mírně zaostával za nejlepším SAT modelem. Nový model pro csp dosáhl nejrychlejších časů v testech s nízkým množstvím překážek a interakcí mezi agenty, zatímco v opačném případě se jeho výkon dramaticky snižoval. Powered by TCPDF (www.tcpdf.org)
|
|
|
DPLL algorithm and propositional proofs
Hrnčiar, Maroš ; Krajíček, Jan (vedoucí práce) ; Koucký, Michal (oponent)
Dôkazová zložitosť je zaujímavá súčasť matematiky nachádzajúca sa na pomedzí obrovskej oblasti logiky a teórie zložitosti. Skúma aké dôkazové systémy sú potrebné na efektívne dokazovanie rôznych matematických tvrdení. Predmetom tejto práce je spojenie medzi dôkazovými systémami a algoritmami na SAT. Uvidíme, že beh algoritmu na nesplniteľnej formule môže byť nahliadnutý ako výrokový dôkaz jej nesplniteľnosti, čím samotný algoritmus prakticky definuje celý dôkazový systém. Práca je určená najmä čitateľom so záujmom o dôkazovú zložitosť, ale dokáže aj samostatne objasniť princíp rezolúcie, či ponúknuť menej obvyklý pohľad na SAT, no zároveň predpokladá čitateľovu znalosť základov výrokovej logiky, teórie grafov a zložitosti.
|
host ::
RSS.